
\section{Automated Safety Preservation}\label{sec:prop_preserv_evol}

We now sequentially present three models of a filesystem which increasingly
satisfy the confidentiality requirements identified in the previous section. 
But first we briefly present the model checker used to evaluate our work.

\subsection{The Model Checker}

In order to help us automating the decision of whether a property is satisfied by a given
model the AlPiNA model checker~\cite{alpina_web} will be used.
AlPiNA uses as models Algebraic Petri Nets. Specifications in
AlPiNA are composed of two parts: an algebraic specification which is a set of
abstract definitions of sorts and associated operations, and a graphical Algebraic Petri Nets representing the model under study.
AlPiNA is able to decide on the satisfaction of
invariant---also called \emph{safety}---properties on those nets. The
invariants are expressed as conditions on the tokens contained by places in the
net at any state of the net's semantics. Invariants are built using first order
logic, the operations defined in the algebraic specification and additional
functions and predicates on the number of tokens contained by places.

\subsection{Naive Filesystem}\label{sec:naive}

Let us start with the first model which we will call \emph{naive filesystem}.
The APN model is depicted in \Fig\ref{fig:naivefs} and represents the
semantics of the operation of a filesystem. The Petri net uses several kinds of
algebraic tokens\footnote{For the presentation of the \emph{confidential
filesystem} example we use in this paper names of sorts and operations which,
despite being self descriptive, for space reasons cannot be formally introduced.
A full description of the algebraic specifications used in the
\emph{confidential filesystem} example can be found in~\cite{lucio:10}.}: pairs
belonging to the set $fileName\times accessClass$ are used in place
\emph{filesystem} to represent file names and their respective access classes;
pairs belonging to the set $userName\times accessClass$ are used in place
\emph{users} to represent a sample of users of the filesystem; finally places
\emph{readFiles} and \emph{writeFiles} hold tokens which are pairs
$(fileName\times accessClass)\times (userName\times accessClass)$ in order to
keep track of which file was opened by which user. We do not explicitly define
the names of the variables that act as weights on the arcs given their type can
be inferred from the either the origin or the target place of the arc.

The semantics of the \emph{naive filesystem} model in \Fig\ref{fig:naivefs}
is such that it simulates opening files in read or write mode and closing them
by firing the \emph{openForRead}, \emph{openForWrite} and \emph{close}
transitions respectively. The variables on the entry arcs of the transitions
declare the consumed tokens from the input places and the variables on the
output arcs of the transitions declare the produced tokens on the output places.
Note that, despite the fact that transitions in APN models may be guarded, in
this naive version of the confidential filesystem the \emph{openForRead} and
\emph{openForWrite} transitions we do not check if the the user has permission to
access a given file.
%
\begin{figure}
	\centering
  \epsfig{file=detailed_material/images/naive_fs, width=\linewidth}
	\caption{Naive filesystem. $M$ defines the initial marking.}
	\label{fig:naivefs}
\end{figure}

Because we have a first formalization of the filesystem, we can now precisely
express the three \emph{confidentiality} requirements we have detailed
informally in \Sect\ref{sec:motivation} as CTL properties. All properties are
safety properties, thus stating what should happen for all states belonging
to the models' semantics and were expressed in AlPiNA syntax for automation
purposes:
\begin{footnotesize}
\begin{eqnarray}
  \forall p \in writeFiles\;.\;userHasPermissionForFile(p) = true\label{conf1}	\\
  \forall p \in readFiles\;.\;userHasPermissionForFile(p) = true\label{conf2}
\end{eqnarray}
\begin{eqnarray}
  &\forall p_r \in readFiles\;.\;(\forall p_w \in writeFiles\;.\;getUserName\nonumber\\
  &(proj_2(p_r)) = getUserName(proj_2(p_w)) =>\nonumber\\
  &(getAccessClass(proj_1(p_r))\nonumber\\
  &dominates\;getAccessClass(proj_1(p_w)) = false&\label{conf3}
\end{eqnarray}
\end{footnotesize}
%
\begin{itemize}
  \item Property~\ref{conf1}, which we will call \emph{respectWritePerms},
  states that a file in the \emph{writeFiles} place has been opened by a user
  who is sufficiently trusted. This decision is computed by the
$userHasPermissionForFile$ predicate which compares the \emph{access class} of
the file with the \emph{access class} of the user who opened it;
  \item Property~\ref{conf2}, which we will call \emph{respectReadPerms}, is
  similar to property~\ref{conf1} but for the files in the \emph{readFiles}
  place; \item Property~\ref{conf3}, which we will call \emph{noReadWriteFlow},
  states that if a user has simultaneously a file open in read mode and
  another in write mode, then the one open in read mode does not $dominate$
  the one open in write mode.
\end{itemize}

\begin{table}
	  \centering
	\caption{Property Satisfaction for the Naive Filesystem}	
	\begin{tabular} {| c | c | c | }
		\hline (\ref{conf1}) respectWritePerms & (\ref{conf2})
		respectReadPerms & (\ref{conf3}) noReadWriteFlow\\ \hline  false & false & false\\
		\hline
	\end{tabular}
	\label{tab:naivefs}
\end{table}
In table~\ref{tab:naivefs} it is possible to observe that the naive filesystem
in \Fig\ref{fig:naivefs} does not respect any of the confidentiality component
properties we have defined. The properties in table~\ref{tab:naivefs} have been
automatically verified using AlPiNA.


\subsection{Simple Security}\label{sec:simple}

The second model which we will call \emph{simple security filesystem} is an
evolution of the \emph{naive filesystem} in \Fig\ref{fig:naivefs} where the
transitions \emph{openForRead} and \emph{openForWrite} become guarded. In
particular, we add to each of those transitions the following guard:

$$dominates(getAccessClass(u), getAccessClass(f))=true$$
where $u\in (userName\times accessClass)$ and $f\in (fileName\times
accessClass)$.

\begin{figure}
	\centering
  \epsfig{file=detailed_material/images/simple_security_fs, width=\linewidth}
	\caption{Simple security filesystem. Same initial marking as \Fig\ref{fig:naivefs}.}
	\label{fig:simplesec}
\end{figure}
%
This means that in the \emph{simple security} model in
\Fig\ref{fig:simplesec} we are enforcing that, in order for a user to read or
write a file, that user has to be sufficiently trusted regarding the
access class of the requested file. This is achieved using the $dominates$
predicate (see~\cite{lucio:10} for the predicate's semantics).
%
\begin{table}
	  \centering
	\caption{Property Satisfaction for the Simple Security Filesystem}		
	\begin{tabular} {| c | c | c | }
		\hline (\ref{conf1}) respectWritePerms & (\ref{conf2})
		respectReadPerms & (\ref{conf3}) noReadWriteFlow\\ \hline
		true & true & false\\
		\hline
	\end{tabular}
	\label{tab:simplesec}
\end{table}

In table~\ref{tab:simplesec} the satisfaction of the confidentiality properties
by the \emph{simple security} model is shown. We can observe that the
introduction of the two guards has rendered confidentiality
properties~\ref{conf1} (respectWritePerms) and~\ref{conf2} (respectReadPerms)
satisfied. In the case of this evolution from the naive filesystem in
figure~\ref{fig:naivefs} into the simple security filesystem in
figure~\ref{fig:simplesec} there are no requirements to preserve, thus there are
no restrictions to the kind of evolution that may occur. However, the evolution
does indeed preserve safety (according to
proposition~\ref{th:safety_preserv_strength}), because there is a place
preserving AHL net morphism between the naive filesystem and the simple security
filesystem nets (due to the fact that the nets are structurally isomorphic) and
the guards in transitions \emph{openForWrite} and \emph{openForRead} are
reinforced.

\subsection{Confinement}\label{sec:confinement}

Finally, we introduce the third model which we will call \emph{confined
filesystem}. The \emph{confined filesystem} model can be observed in
\Fig\ref{fig:confinedfs} and is an evolution of the \emph{simple security
filesystem} in \Fig\ref{fig:simplesec}. Two places \emph{writeFilesLog} and
\emph{readFilesLog} have been added to the APN. The function of these places is
to hold two lists of pairs $(fileName\times accessClass)\times (userName\times
accessClass)$ which log the files which are open for reading and for writing.
When a file is open for reading, a check is done on the \emph{writeFilesLog}
place to decide if there are no files open for writing by the same user which
are less confidential than the file being opened. This is achieved by adding a
condition to the guard of the \emph{openForRead} transition (hidden for lack of
space in \Fig\ref{fig:confinedfs}) as follows:

$$dominates(minAccess(lpw,u), getAccessClass(f))=true$$

where the $minAccess$ function returns the minimum access class value of the set
of files currently open for writing by user $u$.

The $dominates$ predicate is again used to decide if the confidentiality of the
file $f$ being opened by a user $u$ for reading is lower than the minimum
confidentiality of the files opened for writing by user $u$. The reverse
principle is applied to opening files for writing.
%
\begin{figure}[h!]
	\centering
  \epsfig{file=detailed_material/images/confined_fs, width=\linewidth}
	\caption{Confined filesystem. Same initial marking as \Fig\ref{fig:naivefs}.}
	\label{fig:confinedfs}
\end{figure}

If we again model check the confidentiality properties on the new model in
\Fig\ref{fig:confinedfs} we find that the \emph{noReadWriteFlow} property is
now satisfied -- as can be observed in table~\ref{tab:confinedfs}. Note also
that properties~\emph{respectWritePerms} and~\emph{respectReadPerms}
remain true when evolving from the \emph{simple security filesystem} entity to
the \emph{confined filesystem} entity.
%
\begin{table}
	  \centering
	\caption{Property Satisfaction for the Confined Filesystem}		
	\begin{tabular} {| c | c | c | }
		\hline (\ref{conf1}) respectWritePerms & (\ref{conf2})
		respectReadPerms & (\ref{conf3}) noReadWriteFlow\\ \hline
		true & true & true\\
		\hline
	\end{tabular}
	\label{tab:confinedfs}
\end{table}

In the case of this evolution from the simple security filesystem in
figure~\ref{fig:simplesec} into the confined filesystem in
figure~\ref{fig:confinedfs} we need to preserve requirements
(properties)~\ref{conf1} and ~\ref{conf2}. These two requirements
are preserved because there is a guard strengthening AHL net morphism between
the simple security filesystem and the confined filesystem nets. Indeed the two
new places and arcs into existing transitions are allowed by
proposition~\ref{th:safety_preserv_strength}, as well as the additional guard
strengthening made to transitions \emph{openForRead} and \emph{openForWrite}.

In~\cite{lucio:10} we present a complete and rigorous formal description of the
place preserving guard strengthening AHL net morphisms mapping the \emph{naive
filesystem} into the \emph{simple security filesystem} and the \emph{simple
security filesystem} into the \emph{confined filesystem}.


% However, the evolution does indeed preserve safety (according to
% proposition~\ref{th:safety_preserv_strength}), because there is a place
% preserving AHL net morphism between the naive filesystem and the simple security
% filesystem nets (due to the fact that the nets are structurally isomorphic) and
% the guards in transitions \emph{openForWrite} and \emph{openForRead} are
% reinforced.

% Coming back to the three entities we have proposed in \Sect\ref{sec:naive}, we
% can identify two \emph{evolutions}: \emph{naive filesystem} $\rightarrow$
% \emph{simple security filesystem} and \emph{simple security filesystem}
% $\rightarrow$ \emph{confidential filesystem}. We have presented experimental
% evidence that those two evolutions do preserve the safety properties already
% satisfied by the APN model previously to the evolution. In~\cite{lucio:10} we
% present a complete and rigorous formal description of the \emph{place
% preserving} morphisms mapping the \emph{naive filesystem} into the \emph{simple
% security filesystem} and the \emph{simple security filesystem} into the
% \emph{confined filesystem}. The theory in~\cite{Padberg98rule-basedrefinement}
% was not applicable directly to our case study and had to be extended by us to
% allow transition strenghtening of an APN by adding additional guards to an
% existing transition. This extension involved reproving the main theorem of the
% theory with additional hypothesis and the corresponding proof can be found
% in~\cite{lucio:10}.
